$\forall$$T$,$A$:Type, $a$,$x$:Id, $f$:($A$$\rightarrow$$T$), ${\it tg}$:Id, $l$:IdLnk, ${\it es}$:event\_system\{i:l\}. \\[0ex]locl($a$) sends [${\it tg}$,$f$\{$A$$\rightarrow$$T$\}($x$)] on link $l$ once $\in$ prop\{i:l\}